Nuprl Lemma : increasing_implies_le
11,40
postcript
pdf
k
:
,
f
:(int_seg(0;
k
)
).
increasing(
f
;
k
)
guard((
x
,
y
:int_seg(0;
k
). (
x
y
)
((
f
(
x
))
(
f
(
y
)))))
latex
Definitions
t
T
,
guard(
T
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
,
A
,
A
B
,
int_seg(
i
;
j
)
,
,
P
Q
,
decidable(
P
)
,
prop{i:l}
Lemmas
nat
wf
,
increasing
wf
,
int
seg
wf
,
le
wf
,
decidable
int
equal
,
increasing
implies
origin
k:
, f:(int_seg(0; k)
).
guard((x,y:int_seg(0; k). (x 
y) ((f(x)) (f(y))))) k:, f:(int_seg(0; k)).
guard((x,y:int_seg(0; k). (x y) ((f(x)) (f(y))))) 
T Qx:A. B(x)
A B
Q